By introducing the concepts of a loop and a loop formula, Lin and Zhao showed that the answer sets of a nondisjunctive logic program are exactly the models of its Clark's completion that satisfy the loop formulas of all loops. Recently, Gebser and Schaub showed that the Lin-Zhao theorem remains correct even if we restrict loop formulas to a special class of loops called ``elementary loops.'' In this paper, we simplify and generalize the notion of an elementary loop, and clarify its role. We propose the notion of an elementary set, which is almost equivalent to the notion of an elementary loop for nondisjunctive programs, but is simpler, and, unlike elementary loops, can be extended to disjunctive programs without producing unintuitive results. We show that the maximal unfounded elementary sets for the ``relevant'' part of a program are exactly the minimal sets among the nonempty unfounded sets. We also present a graph-theoretic characterization of elementary sets for nondisjunctive programs, which is simpler than the one proposed in (Gebser & Schaub 2005). Unlike the case of nondisjunctive programs, we show that the problem of deciding an elementary set is coNP-complete for disjunctive programs.

This paper proposes an alternative definition of elementary loops and extends the notion of proper loops for disjunctive logic programs. Different from normal logic programs, the computational complexities of recognizing elementary loops and proper loops for disjunctive programs are coNP-complete. To address this problem, we introduce weaker versions of both elementary loops and proper loops and provide polynomial time algorithms for identifying them respectively. On the other hand, based on the notion of elementary loops, the class of Head-Elementary-loop-Free (HEF) programs was presented, which can be turned into equivalent normal logic programs by shifting head atoms into bodies. However, the problem of recognizing an HEF program is coNP-complete. Then we present a subclass of HEF programs which generalizes the class of Head-Cycle-Free programs and provide a polynomial time algorithm to identify them. At last, some experiments show that both elementary loops and proper loops could be replaced by their weak versions in practice.

The notions of loops and loop formulas play an important role in answer set computation. However, there would be an exponential number of loops in the worst case. Gebser and Schaub characterized a subclass elementary loops and showed that they are sufficient for selecting answer sets from models of a logic program. This paper proposes an alternative definition of elementary loops and identify a subclass of elementary loops, called proper loops. By applying a special form of their loop formulas, proper loops are also sufficient for the SAT-based answer set computation. A polynomial algorithm to recognize a proper loop is given and shows that for certain logic programs, identifying all proper loops of a program is more efficient than that of elementary loops. Furthermore, we prove that, by considering the structure of the positive body-head dependency graph of a program, a large number of loops could be ignored for identifying proper loops. We provide another algorithm for identifying all proper loops of a program. The experiments show that, for certain programs whose dependency graphs consisting of sets of components that are densely connected inside and sparsely connected outside, the new algorithm is more efficient.

Using the notion of an elementary loop, Gebser and Schaub refined the theorem on loop formulas due to Lin and Zhao by considering loop formulas of elementary loops only. In this article, we reformulate their definition of an elementary loop, extend it to disjunctive programs, and study several properties of elementary loops, including how maximal elementary loops are related to minimal unfounded sets. The results provide useful insights into the stable model semantics in terms of elementary loops. For a nondisjunctive program, using a graph-theoretic characterization of an elementary loop, we show that the problem of recognizing an elementary loop is tractable. On the other hand, we show that the corresponding problem is {\sf coNP}-complete for a disjunctive program. Based on the notion of an elementary loop, we present the class of Head-Elementary-loop-Free (HEF) programs, which strictly generalizes the class of Head-Cycle-Free (HCF) programs due to Ben-Eliyahu and Dechter. Like an HCF program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head atoms into the body.